YES 2.992
↳ HASKELL
↳ CR
((lookupWithDefaultFM :: FiniteMap Int a -> a -> Int -> a) :: FiniteMap Int a -> a -> Int -> a) |
import qualified Maybe import qualified Prelude |
||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
||||||||||||||||||||||||
lookupFM :: Ord a => FiniteMap a b -> a -> Maybe b
|
||||||||||||||||||||||||
lookupWithDefaultFM :: Ord b => FiniteMap b a -> a -> b -> a
|
import qualified FiniteMap import qualified Prelude |
case lookupFM fm key of Nothing → deflt Just elt → elt
lookupWithDefaultFM0 deflt Nothing = deflt lookupWithDefaultFM0 deflt (Just elt) = elt
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
((lookupWithDefaultFM :: FiniteMap Int a -> a -> Int -> a) :: FiniteMap Int a -> a -> Int -> a) |
import qualified Maybe import qualified Prelude |
||||||||||||||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
||||||||||||||||||||||||
lookupFM :: Ord a => FiniteMap a b -> a -> Maybe b
|
||||||||||||||||||||||||
lookupWithDefaultFM :: Ord a => FiniteMap a b -> b -> a -> b
|
||||||||||||||||||||||||
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
((lookupWithDefaultFM :: FiniteMap Int a -> a -> Int -> a) :: FiniteMap Int a -> a -> Int -> a) |
import qualified Maybe import qualified Prelude |
||||||||||||||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
||||||||||||||||||||||||
lookupFM :: Ord a => FiniteMap a b -> a -> Maybe b
|
||||||||||||||||||||||||
lookupWithDefaultFM :: Ord a => FiniteMap a b -> b -> a -> b
|
||||||||||||||||||||||||
|
import qualified FiniteMap import qualified Prelude |
lookupFM EmptyFM key = Nothing lookupFM (Branch key elt vw fm_l fm_r) key_to_find
| key_to_find < key
= lookupFM fm_l key_to_find | key_to_find > key
= lookupFM fm_r key_to_find | otherwise
= Just elt
lookupFM EmptyFM key = lookupFM4 EmptyFM key lookupFM (Branch key elt vw fm_l fm_r) key_to_find = lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find
lookupFM1 key elt vw fm_l fm_r key_to_find True = lookupFM fm_r key_to_find lookupFM1 key elt vw fm_l fm_r key_to_find False = lookupFM0 key elt vw fm_l fm_r key_to_find otherwise
lookupFM0 key elt vw fm_l fm_r key_to_find True = Just elt
lookupFM2 key elt vw fm_l fm_r key_to_find True = lookupFM fm_l key_to_find lookupFM2 key elt vw fm_l fm_r key_to_find False = lookupFM1 key elt vw fm_l fm_r key_to_find (key_to_find > key)
lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find = lookupFM2 key elt vw fm_l fm_r key_to_find (key_to_find < key)
lookupFM4 EmptyFM key = Nothing lookupFM4 wv ww = lookupFM3 wv ww
undefined
| False
= undefined
undefined = undefined1
undefined0 True = undefined
undefined1 = undefined0 False
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
(lookupWithDefaultFM :: FiniteMap Int a -> a -> Int -> a) |
import qualified Maybe import qualified Prelude |
|||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
|||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
|||||||||
lookupFM :: Ord a => FiniteMap a b -> a -> Maybe b
|
|||||||||
|
|||||||||
|
|||||||||
|
|||||||||
|
|||||||||
|
|||||||||
lookupWithDefaultFM :: Ord a => FiniteMap a b -> b -> a -> b
|
|||||||||
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
new_lookupWithDefaultFM01(wx4, Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Succ(wx500)), bb) → new_lookupWithDefaultFM0(wx4, wx3000, wx31, wx32, wx33, wx34, wx500, wx500, wx3000, bb)
new_lookupWithDefaultFM02(wx80, wx81, wx82, wx83, wx84, wx85, wx86, h) → new_lookupWithDefaultFM00(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Succ(wx86), Succ(wx81), h)
new_lookupWithDefaultFM0(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Succ(wx870), Succ(wx880), h) → new_lookupWithDefaultFM0(wx80, wx81, wx82, wx83, wx84, wx85, wx86, wx870, wx880, h)
new_lookupWithDefaultFM00(wx174, wx175, wx176, wx177, wx178, wx179, wx180, Succ(wx1810), Succ(wx1820), ba) → new_lookupWithDefaultFM00(wx174, wx175, wx176, wx177, wx178, wx179, wx180, wx1810, wx1820, ba)
new_lookupWithDefaultFM0(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Succ(wx870), Zero, h) → new_lookupWithDefaultFM00(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Succ(wx86), Succ(wx81), h)
new_lookupWithDefaultFM03(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Succ(wx970), Succ(wx980), bc) → new_lookupWithDefaultFM03(wx90, wx91, wx92, wx93, wx94, wx95, wx96, wx970, wx980, bc)
new_lookupWithDefaultFM03(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Zero, Succ(wx980), bc) → new_lookupWithDefaultFM01(wx90, wx94, Neg(Succ(wx96)), bc)
new_lookupWithDefaultFM03(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Succ(wx970), Zero, bc) → new_lookupWithDefaultFM04(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Succ(wx91), Succ(wx96), bc)
new_lookupWithDefaultFM01(wx4, Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Succ(wx500)), bb) → new_lookupWithDefaultFM03(wx4, wx3000, wx31, wx32, wx33, wx34, wx500, wx3000, wx500, bb)
new_lookupWithDefaultFM0(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Zero, Zero, h) → new_lookupWithDefaultFM02(wx80, wx81, wx82, wx83, wx84, wx85, wx86, h)
new_lookupWithDefaultFM01(wx4, Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Zero), bb) → new_lookupWithDefaultFM01(wx4, wx33, Neg(Zero), bb)
new_lookupWithDefaultFM01(wx4, Branch(Pos(Zero), wx31, wx32, wx33, wx34), Pos(Succ(wx500)), bb) → new_lookupWithDefaultFM01(wx4, wx34, Pos(Succ(wx500)), bb)
new_lookupWithDefaultFM01(wx4, Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Zero), bb) → new_lookupWithDefaultFM01(wx4, wx33, Pos(Zero), bb)
new_lookupWithDefaultFM04(wx184, wx185, wx186, wx187, wx188, wx189, wx190, Succ(wx1910), Zero, bd) → new_lookupWithDefaultFM01(wx184, wx189, Neg(Succ(wx190)), bd)
new_lookupWithDefaultFM01(wx4, Branch(Neg(wx300), wx31, wx32, wx33, wx34), Pos(Succ(wx500)), bb) → new_lookupWithDefaultFM01(wx4, wx34, Pos(Succ(wx500)), bb)
new_lookupWithDefaultFM0(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Zero, Succ(wx880), h) → new_lookupWithDefaultFM01(wx80, wx84, Pos(Succ(wx86)), h)
new_lookupWithDefaultFM05(wx90, wx91, wx92, wx93, wx94, wx95, wx96, bc) → new_lookupWithDefaultFM04(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Succ(wx91), Succ(wx96), bc)
new_lookupWithDefaultFM00(wx174, wx175, wx176, wx177, wx178, wx179, wx180, Succ(wx1810), Zero, ba) → new_lookupWithDefaultFM01(wx174, wx179, Pos(Succ(wx180)), ba)
new_lookupWithDefaultFM03(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Zero, Zero, bc) → new_lookupWithDefaultFM05(wx90, wx91, wx92, wx93, wx94, wx95, wx96, bc)
new_lookupWithDefaultFM04(wx184, wx185, wx186, wx187, wx188, wx189, wx190, Succ(wx1910), Succ(wx1920), bd) → new_lookupWithDefaultFM04(wx184, wx185, wx186, wx187, wx188, wx189, wx190, wx1910, wx1920, bd)
new_lookupWithDefaultFM01(wx4, Branch(Neg(Zero), wx31, wx32, wx33, wx34), Neg(Succ(wx500)), bb) → new_lookupWithDefaultFM01(wx4, wx33, Neg(Succ(wx500)), bb)
new_lookupWithDefaultFM01(wx4, Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Zero), bb) → new_lookupWithDefaultFM01(wx4, wx34, Neg(Zero), bb)
new_lookupWithDefaultFM01(wx4, Branch(Pos(wx300), wx31, wx32, wx33, wx34), Neg(Succ(wx500)), bb) → new_lookupWithDefaultFM01(wx4, wx33, Neg(Succ(wx500)), bb)
new_lookupWithDefaultFM01(wx4, Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Zero), bb) → new_lookupWithDefaultFM01(wx4, wx34, Pos(Zero), bb)
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
new_lookupWithDefaultFM01(wx4, Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Zero), bb) → new_lookupWithDefaultFM01(wx4, wx33, Pos(Zero), bb)
new_lookupWithDefaultFM01(wx4, Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Zero), bb) → new_lookupWithDefaultFM01(wx4, wx34, Pos(Zero), bb)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
new_lookupWithDefaultFM01(wx4, Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Zero), bb) → new_lookupWithDefaultFM01(wx4, wx33, Neg(Zero), bb)
new_lookupWithDefaultFM01(wx4, Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Zero), bb) → new_lookupWithDefaultFM01(wx4, wx34, Neg(Zero), bb)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
new_lookupWithDefaultFM04(wx184, wx185, wx186, wx187, wx188, wx189, wx190, Succ(wx1910), Zero, bd) → new_lookupWithDefaultFM01(wx184, wx189, Neg(Succ(wx190)), bd)
new_lookupWithDefaultFM05(wx90, wx91, wx92, wx93, wx94, wx95, wx96, bc) → new_lookupWithDefaultFM04(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Succ(wx91), Succ(wx96), bc)
new_lookupWithDefaultFM03(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Succ(wx970), Succ(wx980), bc) → new_lookupWithDefaultFM03(wx90, wx91, wx92, wx93, wx94, wx95, wx96, wx970, wx980, bc)
new_lookupWithDefaultFM03(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Succ(wx970), Zero, bc) → new_lookupWithDefaultFM04(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Succ(wx91), Succ(wx96), bc)
new_lookupWithDefaultFM03(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Zero, Succ(wx980), bc) → new_lookupWithDefaultFM01(wx90, wx94, Neg(Succ(wx96)), bc)
new_lookupWithDefaultFM03(wx90, wx91, wx92, wx93, wx94, wx95, wx96, Zero, Zero, bc) → new_lookupWithDefaultFM05(wx90, wx91, wx92, wx93, wx94, wx95, wx96, bc)
new_lookupWithDefaultFM04(wx184, wx185, wx186, wx187, wx188, wx189, wx190, Succ(wx1910), Succ(wx1920), bd) → new_lookupWithDefaultFM04(wx184, wx185, wx186, wx187, wx188, wx189, wx190, wx1910, wx1920, bd)
new_lookupWithDefaultFM01(wx4, Branch(Neg(Zero), wx31, wx32, wx33, wx34), Neg(Succ(wx500)), bb) → new_lookupWithDefaultFM01(wx4, wx33, Neg(Succ(wx500)), bb)
new_lookupWithDefaultFM01(wx4, Branch(Neg(Succ(wx3000)), wx31, wx32, wx33, wx34), Neg(Succ(wx500)), bb) → new_lookupWithDefaultFM03(wx4, wx3000, wx31, wx32, wx33, wx34, wx500, wx3000, wx500, bb)
new_lookupWithDefaultFM01(wx4, Branch(Pos(wx300), wx31, wx32, wx33, wx34), Neg(Succ(wx500)), bb) → new_lookupWithDefaultFM01(wx4, wx33, Neg(Succ(wx500)), bb)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
new_lookupWithDefaultFM01(wx4, Branch(Pos(Succ(wx3000)), wx31, wx32, wx33, wx34), Pos(Succ(wx500)), bb) → new_lookupWithDefaultFM0(wx4, wx3000, wx31, wx32, wx33, wx34, wx500, wx500, wx3000, bb)
new_lookupWithDefaultFM01(wx4, Branch(Pos(Zero), wx31, wx32, wx33, wx34), Pos(Succ(wx500)), bb) → new_lookupWithDefaultFM01(wx4, wx34, Pos(Succ(wx500)), bb)
new_lookupWithDefaultFM02(wx80, wx81, wx82, wx83, wx84, wx85, wx86, h) → new_lookupWithDefaultFM00(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Succ(wx86), Succ(wx81), h)
new_lookupWithDefaultFM01(wx4, Branch(Neg(wx300), wx31, wx32, wx33, wx34), Pos(Succ(wx500)), bb) → new_lookupWithDefaultFM01(wx4, wx34, Pos(Succ(wx500)), bb)
new_lookupWithDefaultFM0(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Zero, Succ(wx880), h) → new_lookupWithDefaultFM01(wx80, wx84, Pos(Succ(wx86)), h)
new_lookupWithDefaultFM0(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Succ(wx870), Succ(wx880), h) → new_lookupWithDefaultFM0(wx80, wx81, wx82, wx83, wx84, wx85, wx86, wx870, wx880, h)
new_lookupWithDefaultFM00(wx174, wx175, wx176, wx177, wx178, wx179, wx180, Succ(wx1810), Succ(wx1820), ba) → new_lookupWithDefaultFM00(wx174, wx175, wx176, wx177, wx178, wx179, wx180, wx1810, wx1820, ba)
new_lookupWithDefaultFM0(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Succ(wx870), Zero, h) → new_lookupWithDefaultFM00(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Succ(wx86), Succ(wx81), h)
new_lookupWithDefaultFM00(wx174, wx175, wx176, wx177, wx178, wx179, wx180, Succ(wx1810), Zero, ba) → new_lookupWithDefaultFM01(wx174, wx179, Pos(Succ(wx180)), ba)
new_lookupWithDefaultFM0(wx80, wx81, wx82, wx83, wx84, wx85, wx86, Zero, Zero, h) → new_lookupWithDefaultFM02(wx80, wx81, wx82, wx83, wx84, wx85, wx86, h)
From the DPs we obtained the following set of size-change graphs: